<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>RecordSub: Subtyping with Records</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 2: Programming Language Foundations</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>Table of Contents</li></a>
   <a href='coqindex.html'><li class='section_name'>Index</li></a>
   <a href='deps.html'><li class='section_name'>Roadmap</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">RecordSub<span class="subtitle">Subtyping with Records</span></h1>


<div class="doc">

<div class="paragraph"> </div>

 In this chapter, we combine two significant extensions of the pure
    STLC &mdash; records (from chapter <a href="Records.html"><span class="inlineref">Records</span></a>) and subtyping (from
    chapter <a href="Sub.html"><span class="inlineref">Sub</span></a>) &mdash; and explore their interactions.  Most of the
    concepts have already been discussed in those chapters, so the
    presentation here is somewhat terse.  We just comment where things
    are nonstandard. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Set</span> <span class="id" type="var">Warnings</span> "-notation-overridden,-parsing".<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Strings.String</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Maps</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Smallstep</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">MoreStlc</span>.<br/>
</div>

<div class="doc">
<a name="lab401"></a><h1 class="section">Core Definitions</h1>

</div>
<div class="code code-space">

<br/>
</div>

<div class="doc">
<a name="lab402"></a><h3 class="section">Syntax</h3>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">ty</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;proper&nbsp;types&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Top</span>   : <span class="id" type="var">ty</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Base</span>  : <span class="id" type="var">string</span> → <span class="id" type="var">ty</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Arrow</span> : <span class="id" type="var">ty</span> → <span class="id" type="var">ty</span> → <span class="id" type="var">ty</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;record&nbsp;types&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">RNil</span> : <span class="id" type="var">ty</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">RCons</span> : <span class="id" type="var">string</span> → <span class="id" type="var">ty</span> → <span class="id" type="var">ty</span> → <span class="id" type="var">ty</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">tm</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;proper&nbsp;terms&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">var</span> : <span class="id" type="var">string</span> → <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">app</span> : <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">abs</span> : <span class="id" type="var">string</span> → <span class="id" type="var">ty</span> → <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">rproj</span> : <span class="id" type="var">tm</span> → <span class="id" type="var">string</span> → <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;record&nbsp;terms&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">rnil</span> :  <span class="id" type="var">tm</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">rcons</span> : <span class="id" type="var">string</span> → <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span>.<br/>
</div>

<div class="doc">
<a name="lab403"></a><h3 class="section">Well-Formedness</h3>

<div class="paragraph"> </div>

 The syntax of terms and types is a bit too loose, in the sense
    that it admits things like a record type whose final "tail" is
    <span class="inlinecode"><span class="id" type="var">Top</span></span> or some arrow type rather than <span class="inlinecode"><span class="id" type="var">Nil</span></span>.  To avoid such cases,
    it is useful to assume that all the record types and terms that we
    see will obey some simple well-formedness conditions.

<div class="paragraph"> </div>

    <span class="inlinecode"><span class="id" type="var">An</span></span> <span class="inlinecode"><span class="id" type="var">interesting</span></span> <span class="inlinecode"><span class="id" type="var">technical</span></span> <span class="inlinecode"><span class="id" type="var">question</span></span> <span class="inlinecode"><span class="id" type="var">is</span></span> <span class="inlinecode"><span class="id" type="var">whether</span></span> <span class="inlinecode"><span class="id" type="var">the</span></span> <span class="inlinecode"><span class="id" type="var">basic</span></span> <span class="inlinecode"><span class="id" type="var">properties</span></span>
    <span class="inlinecode"><span class="id" type="var">of</span></span> <span class="inlinecode"><span class="id" type="var">the</span></span> <span class="inlinecode"><span class="id" type="var">system</span></span> <span class="inlinecode">--</span> <span class="inlinecode"><span class="id" type="tactic">progress</span></span> <span class="inlinecode"><span class="id" type="var">and</span></span> <span class="inlinecode"><span class="id" type="var">preservation</span></span> <span class="inlinecode">--</span> <span class="inlinecode"><span class="id" type="var">remain</span></span> <span class="inlinecode"><span class="id" type="var">true</span></span> <span class="inlinecode"><span class="id" type="keyword">if</span></span> <span class="inlinecode"><span class="id" type="var">we</span></span>
    <span class="inlinecode"><span class="id" type="var">drop</span></span> <span class="inlinecode"><span class="id" type="var">these</span></span> <span class="inlinecode"><span class="id" type="var">conditions</span>.</span>  <span class="inlinecode"><span class="id" type="var">I</span></span> <span class="inlinecode"><span class="id" type="var">believe</span></span> <span class="inlinecode"><span class="id" type="var">they</span></span> <span class="inlinecode"><span class="id" type="tactic">do</span>,</span> <span class="inlinecode"><span class="id" type="var">and</span></span> <span class="inlinecode"><span class="id" type="var">I</span></span> <span class="inlinecode"><span class="id" type="var">would</span></span> <span class="inlinecode"><span class="id" type="var">encourage</span></span>
    <span class="inlinecode"><span class="id" type="var">motivated</span></span> <span class="inlinecode"><span class="id" type="var">readers</span></span> <span class="inlinecode"><span class="id" type="var">to</span></span> <span class="inlinecode"><span class="id" type="tactic">try</span></span> <span class="inlinecode"><span class="id" type="var">to</span></span> <span class="inlinecode"><span class="id" type="var">check</span></span> <span class="inlinecode"><span class="id" type="var">this</span></span> <span class="inlinecode"><span class="id" type="tactic">by</span></span> <span class="inlinecode"><span class="id" type="var">dropping</span></span> <span class="inlinecode"><span class="id" type="var">the</span></span> <span class="inlinecode"><span class="id" type="var">conditions</span></span>
    <span class="inlinecode"><span class="id" type="var">from</span></span> <span class="inlinecode"><span class="id" type="var">the</span></span> <span class="inlinecode"><span class="id" type="var">definitions</span></span> <span class="inlinecode"><span class="id" type="var">of</span></span> <span class="inlinecode"><span class="id" type="var">typing</span></span> <span class="inlinecode"><span class="id" type="var">and</span></span> <span class="inlinecode"><span class="id" type="var">subtyping</span></span> <span class="inlinecode"><span class="id" type="var">and</span></span> <span class="inlinecode"><span class="id" type="var">adjusting</span></span> <span class="inlinecode"><span class="id" type="var">the</span></span>
    <span class="inlinecode"><span class="id" type="var">proofs</span></span> <span class="inlinecode"><span class="id" type="keyword">in</span></span> <span class="inlinecode"><span class="id" type="var">the</span></span> <span class="inlinecode"><span class="id" type="var">rest</span></span> <span class="inlinecode"><span class="id" type="var">of</span></span> <span class="inlinecode"><span class="id" type="var">the</span></span> <span class="inlinecode"><span class="id" type="var">chapter</span></span> <span class="inlinecode"><span class="id" type="var">accordingly</span>.</span>  <span class="inlinecode"><span class="id" type="var">This</span></span> <span class="inlinecode"><span class="id" type="var">is</span></span> <span class="inlinecode"><span class="id" type="var">not</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span>
    <span class="inlinecode"><span class="id" type="tactic">trivial</span></span> <span class="inlinecode"><span class="id" type="var">exercise</span></span> <span class="inlinecode">(<span class="id" type="var">or</span></span> <span class="inlinecode"><span class="id" type="var">I'd</span></span> <span class="inlinecode"><span class="id" type="var">have</span></span> <span class="inlinecode"><span class="id" type="var">done</span></span> <span class="inlinecode"><span class="id" type="var">it</span>!),</span> <span class="inlinecode"><span class="id" type="var">but</span></span> <span class="inlinecode"><span class="id" type="var">it</span></span> <span class="inlinecode"><span class="id" type="var">should</span></span> <span class="inlinecode"><span class="id" type="var">not</span></span> <span class="inlinecode"><span class="id" type="var">involve</span></span>
    <span class="inlinecode"><span class="id" type="var">changing</span></span> <span class="inlinecode"><span class="id" type="var">the</span></span> <span class="inlinecode"><span class="id" type="var">basic</span></span> <span class="inlinecode"><span class="id" type="var">structure</span></span> <span class="inlinecode"><span class="id" type="var">of</span></span> <span class="inlinecode"><span class="id" type="var">the</span></span> <span class="inlinecode"><span class="id" type="var">proofs</span>.</span>  <span class="inlinecode"><span class="id" type="var">If</span></span> <span class="inlinecode"><span class="id" type="var">someone</span></span> <span class="inlinecode"><span class="id" type="var">does</span></span> <span class="inlinecode"><span class="id" type="tactic">do</span></span>
    <span class="inlinecode"><span class="id" type="var">it</span>,</span> <span class="inlinecode"><span class="id" type="var">please</span></span> <span class="inlinecode"><span class="id" type="keyword">let</span></span> <span class="inlinecode"><span class="id" type="var">me</span></span> <span class="inlinecode"><span class="id" type="var">know</span>.</span> <span class="inlinecode">--<span class="id" type="var">BCP</span></span> <span class="inlinecode">5/16.</span> 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">record_ty</span> : <span class="id" type="var">ty</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">RTnil</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">record_ty</span> <span class="id" type="var">RNil</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">RTcons</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">i</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">record_ty</span> (<span class="id" type="var">RCons</span> <span class="id" type="var">i</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">record_tm</span> : <span class="id" type="var">tm</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">rtnil</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">record_tm</span> <span class="id" type="var">rnil</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">rtcons</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">i</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">record_tm</span> (<span class="id" type="var">rcons</span> <span class="id" type="var">i</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">well_formed_ty</span> : <span class="id" type="var">ty</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">wfTop</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> <span class="id" type="var">Top</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">wfBase</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">i</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> (<span class="id" type="var">Base</span> <span class="id" type="var">i</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">wfArrow</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> <span class="id" type="var">T<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> <span class="id" type="var">T<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">wfRNil</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> <span class="id" type="var">RNil</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">wfRCons</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">i</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> <span class="id" type="var">T<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> <span class="id" type="var">T<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">record_ty</span> <span class="id" type="var">T<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> (<span class="id" type="var">RCons</span> <span class="id" type="var">i</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">record_ty</span> <span class="id" type="var">record_tm</span> <span class="id" type="var">well_formed_ty</span>.<br/>
</div>

<div class="doc">
<a name="lab404"></a><h3 class="section">Substitution</h3>

<div class="paragraph"> </div>

 Substitution and reduction are as before. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="tactic">subst</span> (<span class="id" type="var">x</span>:<span class="id" type="var">string</span>) (<span class="id" type="var">s</span>:<span class="id" type="var">tm</span>) (<span class="id" type="var">t</span>:<span class="id" type="var">tm</span>) : <span class="id" type="var">tm</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">var</span> <span class="id" type="var">y</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">eqb_string</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="keyword">then</span> <span class="id" type="var">s</span> <span class="id" type="keyword">else</span> <span class="id" type="var">t</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">abs</span> <span class="id" type="var">y</span> <span class="id" type="var">T</span> <span class="id" type="var">t<sub>1</sub></span> ⇒  <span class="id" type="var">abs</span> <span class="id" type="var">y</span> <span class="id" type="var">T</span> (<span class="id" type="keyword">if</span> <span class="id" type="var">eqb_string</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="keyword">then</span> <span class="id" type="var">t<sub>1</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t<sub>1</sub></span>))<br/>
&nbsp;&nbsp;| <span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> ⇒ <span class="id" type="var">app</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t<sub>1</sub></span>) (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">rproj</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">i</span> ⇒ <span class="id" type="var">rproj</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t<sub>1</sub></span>) <span class="id" type="var">i</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">rnil</span> ⇒ <span class="id" type="var">rnil</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">rcons</span> <span class="id" type="var">i</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">tr<sub>2</sub></span> ⇒ <span class="id" type="var">rcons</span> <span class="id" type="var">i</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t<sub>1</sub></span>) (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">tr<sub>2</sub></span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Notation</span> "'[' x ':=' s ']' t" := (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 20).<br/>
</div>

<div class="doc">
<a name="lab405"></a><h3 class="section">Reduction</h3>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">value</span> : <span class="id" type="var">tm</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">v_abs</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">T</span> <span class="id" type="var">t</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> (<span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">T</span> <span class="id" type="var">t</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">v_rnil</span> : <span class="id" type="var">value</span> <span class="id" type="var">rnil</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">v_rcons</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">i</span> <span class="id" type="var">v</span> <span class="id" type="var">vr</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">v</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">vr</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> (<span class="id" type="var">rcons</span> <span class="id" type="var">i</span> <span class="id" type="var">v</span> <span class="id" type="var">vr</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">value</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">Tlookup</span> (<span class="id" type="var">i</span>:<span class="id" type="var">string</span>) (<span class="id" type="var">Tr</span>:<span class="id" type="var">ty</span>) : <span class="id" type="var">option</span> <span class="id" type="var">ty</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">Tr</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">RCons</span> <span class="id" type="var">i'</span> <span class="id" type="var">T</span> <span class="id" type="var">Tr'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">if</span> <span class="id" type="var">eqb_string</span> <span class="id" type="var">i</span> <span class="id" type="var">i'</span> <span class="id" type="keyword">then</span> <span class="id" type="var">Some</span> <span class="id" type="var">T</span> <span class="id" type="keyword">else</span> <span class="id" type="var">Tlookup</span> <span class="id" type="var">i</span> <span class="id" type="var">Tr'</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">_</span> ⇒ <span class="id" type="var">None</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">tlookup</span> (<span class="id" type="var">i</span>:<span class="id" type="var">string</span>) (<span class="id" type="var">tr</span>:<span class="id" type="var">tm</span>) : <span class="id" type="var">option</span> <span class="id" type="var">tm</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">tr</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">rcons</span> <span class="id" type="var">i'</span> <span class="id" type="var">t</span> <span class="id" type="var">tr'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">if</span> <span class="id" type="var">eqb_string</span> <span class="id" type="var">i</span> <span class="id" type="var">i'</span> <span class="id" type="keyword">then</span> <span class="id" type="var">Some</span> <span class="id" type="var">t</span> <span class="id" type="keyword">else</span> <span class="id" type="var">tlookup</span> <span class="id" type="var">i</span> <span class="id" type="var">tr'</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">_</span> ⇒ <span class="id" type="var">None</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Reserved Notation</span> "t<sub>1</sub> '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>' t<sub>2</sub>" (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">step</span> : <span class="id" type="var">tm</span> → <span class="id" type="var">tm</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_AppAbs</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">T</span> <span class="id" type="var">t<sub>12</sub></span> <span class="id" type="var">v<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">v<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">app</span> (<span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">T</span> <span class="id" type="var">t<sub>12</sub></span>) <span class="id" type="var">v<sub>2</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [<span class="id" type="var">x</span>:=<span class="id" type="var">v<sub>2</sub></span>]<span class="id" type="var">t<sub>12</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_App1</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">t<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t<sub>1</sub></span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t<sub>1</sub>'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">t<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_App2</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">v<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>2</sub>'</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">v<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t<sub>2</sub></span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t<sub>2</sub>'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">app</span> <span class="id" type="var">v<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (<span class="id" type="var">app</span> <span class="id" type="var">v<sub>1</sub></span>  <span class="id" type="var">t<sub>2</sub>'</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_Proj1</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">tr</span> <span class="id" type="var">tr'</span> <span class="id" type="var">i</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">tr</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">tr'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">rproj</span> <span class="id" type="var">tr</span> <span class="id" type="var">i</span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (<span class="id" type="var">rproj</span> <span class="id" type="var">tr'</span> <span class="id" type="var">i</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_ProjRcd</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">tr</span> <span class="id" type="var">i</span> <span class="id" type="var">vi</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">tr</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">tlookup</span> <span class="id" type="var">i</span> <span class="id" type="var">tr</span> = <span class="id" type="var">Some</span> <span class="id" type="var">vi</span>    →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">rproj</span> <span class="id" type="var">tr</span> <span class="id" type="var">i</span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">vi</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_Rcd_Head</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">i</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">tr<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t<sub>1</sub></span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t<sub>1</sub>'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">rcons</span> <span class="id" type="var">i</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">tr<sub>2</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (<span class="id" type="var">rcons</span> <span class="id" type="var">i</span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">tr<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">ST_Rcd_Tail</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">i</span> <span class="id" type="var">v<sub>1</sub></span> <span class="id" type="var">tr<sub>2</sub></span> <span class="id" type="var">tr<sub>2</sub>'</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">v<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">tr<sub>2</sub></span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">tr<sub>2</sub>'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">rcons</span> <span class="id" type="var">i</span> <span class="id" type="var">v<sub>1</sub></span> <span class="id" type="var">tr<sub>2</sub></span>) <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (<span class="id" type="var">rcons</span> <span class="id" type="var">i</span> <span class="id" type="var">v<sub>1</sub></span> <span class="id" type="var">tr<sub>2</sub>'</span>)<br/>
<br/>
<span class="id" type="keyword">where</span> "t<sub>1</sub> '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>' t<sub>2</sub>" := (<span class="id" type="var">step</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">step</span>.<br/>
</div>

<div class="doc">
<a name="lab406"></a><h1 class="section">Subtyping</h1>

<div class="paragraph"> </div>

 Now we come to the interesting part, where the features we've
    added start to interact.  We begin by defining the subtyping
    relation and developing some of its important technical
    properties. 
</div>

<div class="doc">
<a name="lab407"></a><h2 class="section">Definition</h2>

<div class="paragraph"> </div>

 The definition of subtyping is essentially just what we sketched
    in the discussion of record subtyping in chapter <a href="Sub.html"><span class="inlineref">Sub</span></a>, but we
    need to add well-formedness side conditions to some of the rules.
    Also, we replace the "n-ary" width, depth, and permutation
    subtyping rules by binary rules that deal with just the first
    field. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Reserved Notation</span> "T '&lt;:' U" (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">subtype</span> : <span class="id" type="var">ty</span> → <span class="id" type="var">ty</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Subtyping&nbsp;between&nbsp;proper&nbsp;types&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">S_Refl</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">T</span> &lt;: <span class="id" type="var">T</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">S_Trans</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">S</span> <span class="id" type="var">U</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span> &lt;: <span class="id" type="var">U</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">U</span> &lt;: <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span> &lt;: <span class="id" type="var">T</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">S_Top</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">S</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> <span class="id" type="var">S</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S</span> &lt;: <span class="id" type="var">Top</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">S_Arrow</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">S<sub>2</sub></span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">T<sub>1</sub></span> &lt;: <span class="id" type="var">S<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S<sub>2</sub></span> &lt;: <span class="id" type="var">T<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Arrow</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">S<sub>2</sub></span> &lt;: <span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Subtyping&nbsp;between&nbsp;record&nbsp;types&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">S_RcdWidth</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">i</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> (<span class="id" type="var">RCons</span> <span class="id" type="var">i</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">RCons</span> <span class="id" type="var">i</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span> &lt;: <span class="id" type="var">RNil</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">S_RcdDepth</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">i</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">Sr<sub>2</sub></span> <span class="id" type="var">Tr<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">S<sub>1</sub></span> &lt;: <span class="id" type="var">T<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Sr<sub>2</sub></span> &lt;: <span class="id" type="var">Tr<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">record_ty</span> <span class="id" type="var">Sr<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">record_ty</span> <span class="id" type="var">Tr<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">RCons</span> <span class="id" type="var">i</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">Sr<sub>2</sub></span> &lt;: <span class="id" type="var">RCons</span> <span class="id" type="var">i</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">Tr<sub>2</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">S_RcdPerm</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">i<sub>1</sub></span> <span class="id" type="var">i<sub>2</sub></span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span> <span class="id" type="var">Tr<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> (<span class="id" type="var">RCons</span> <span class="id" type="var">i<sub>1</sub></span> <span class="id" type="var">T<sub>1</sub></span> (<span class="id" type="var">RCons</span> <span class="id" type="var">i<sub>2</sub></span> <span class="id" type="var">T<sub>2</sub></span> <span class="id" type="var">Tr<sub>3</sub></span>)) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">i<sub>1</sub></span> ≠ <span class="id" type="var">i<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">RCons</span> <span class="id" type="var">i<sub>1</sub></span> <span class="id" type="var">T<sub>1</sub></span> (<span class="id" type="var">RCons</span> <span class="id" type="var">i<sub>2</sub></span> <span class="id" type="var">T<sub>2</sub></span> <span class="id" type="var">Tr<sub>3</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&lt;: <span class="id" type="var">RCons</span> <span class="id" type="var">i<sub>2</sub></span> <span class="id" type="var">T<sub>2</sub></span> (<span class="id" type="var">RCons</span> <span class="id" type="var">i<sub>1</sub></span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">Tr<sub>3</sub></span>)<br/>
<br/>
<span class="id" type="keyword">where</span> "T '&lt;:' U" := (<span class="id" type="var">subtype</span> <span class="id" type="var">T</span> <span class="id" type="var">U</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">subtype</span>.<br/>
</div>

<div class="doc">
<a name="lab408"></a><h2 class="section">Examples</h2>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">Examples</span>.<br/>
<span class="id" type="keyword">Open</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">string_scope</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">x</span> := "x".<br/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">y</span> := "y".<br/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">z</span> := "z".<br/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">j</span> := "j".<br/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">k</span> := "k".<br/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">i</span> := "i".<br/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">A</span> := (<span class="id" type="var">Base</span> "A").<br/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">B</span> := (<span class="id" type="var">Base</span> "B").<br/>
<span class="id" type="keyword">Notation</span> <span class="id" type="var">C</span> := (<span class="id" type="var">Base</span> "C").<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">TRcd_j</span>  :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">RCons</span> <span class="id" type="var">j</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">B</span> <span class="id" type="var">B</span>) <span class="id" type="var">RNil</span>). <span class="comment">(*&nbsp;{j:B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B}&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">TRcd_kj</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">RCons</span> <span class="id" type="var">k</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">A</span> <span class="id" type="var">A</span>) <span class="id" type="var">TRcd_j</span>. <span class="comment">(*&nbsp;{k:C<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>C,j:B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B}&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">subtyping_example_0</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">subtype</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">C</span> <span class="id" type="var">TRcd_kj</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">Arrow</span> <span class="id" type="var">C</span> <span class="id" type="var">RNil</span>).<br/>
<span class="comment">(*&nbsp;C<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>{k:A<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>A,j:B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B}&nbsp;&lt;:&nbsp;C<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>{}&nbsp;*)</span><br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">S_Arrow</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">S_Refl</span>. <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">TRcd_kj</span>, <span class="id" type="var">TRcd_j</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">S_RcdWidth</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The following facts are mostly easy to prove in Coq.  To get full
    benefit, make sure you also understand how to prove them on
    paper! 
<div class="paragraph"> </div>

<a name="lab409"></a><h4 class="section">Exercise: 2 stars, standard (subtyping_example_1)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Example</span> <span class="id" type="var">subtyping_example_1</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">TRcd_kj</span> <span class="id" type="var">TRcd_j</span>.<br/>
<span class="comment">(*&nbsp;{k:A<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>A,j:B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B}&nbsp;&lt;:&nbsp;{j:B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B}&nbsp;*)</span><br/>
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab410"></a><h4 class="section">Exercise: 1 star, standard (subtyping_example_2)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Example</span> <span class="id" type="var">subtyping_example_2</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">subtype</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">Top</span> <span class="id" type="var">TRcd_kj</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">Arrow</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">C</span> <span class="id" type="var">C</span>) <span class="id" type="var">TRcd_j</span>).<br/>
<span class="comment">(*&nbsp;Top<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>{k:A<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>A,j:B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B}&nbsp;&lt;:&nbsp;(C<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>C)<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>{j:B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B}&nbsp;*)</span><br/>
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab411"></a><h4 class="section">Exercise: 1 star, standard (subtyping_example_3)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Example</span> <span class="id" type="var">subtyping_example_3</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">subtype</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">RNil</span> (<span class="id" type="var">RCons</span> <span class="id" type="var">j</span> <span class="id" type="var">A</span> <span class="id" type="var">RNil</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">Arrow</span> (<span class="id" type="var">RCons</span> <span class="id" type="var">k</span> <span class="id" type="var">B</span> <span class="id" type="var">RNil</span>) <span class="id" type="var">RNil</span>).<br/>
<span class="comment">(*&nbsp;{}<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>{j:A}&nbsp;&lt;:&nbsp;{k:B}<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>{}&nbsp;*)</span><br/>
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab412"></a><h4 class="section">Exercise: 2 stars, standard (subtyping_example_4)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Example</span> <span class="id" type="var">subtyping_example_4</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">subtype</span> (<span class="id" type="var">RCons</span> <span class="id" type="var">x</span> <span class="id" type="var">A</span> (<span class="id" type="var">RCons</span> <span class="id" type="var">y</span> <span class="id" type="var">B</span> (<span class="id" type="var">RCons</span> <span class="id" type="var">z</span> <span class="id" type="var">C</span> <span class="id" type="var">RNil</span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">RCons</span> <span class="id" type="var">z</span> <span class="id" type="var">C</span> (<span class="id" type="var">RCons</span> <span class="id" type="var">y</span> <span class="id" type="var">B</span> (<span class="id" type="var">RCons</span> <span class="id" type="var">x</span> <span class="id" type="var">A</span> <span class="id" type="var">RNil</span>))).<br/>
<span class="comment">(*&nbsp;{x:A,y:B,z:C}&nbsp;&lt;:&nbsp;{z:C,y:B,x:A}&nbsp;*)</span><br/>
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">Examples</span>.<br/>
</div>

<div class="doc">
<a name="lab413"></a><h2 class="section">Properties of Subtyping</h2>

<div class="paragraph"> </div>

<a name="lab414"></a><h3 class="section">Well-Formedness</h3>

<div class="paragraph"> </div>

 To get started proving things about subtyping, we need a couple of
    technical lemmas that intuitively (1) allow us to extract the
    well-formedness assumptions embedded in subtyping derivations
    and (2) record the fact that fields of well-formed record types
    are themselves well-formed types.  
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">subtype__wf</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">S</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">S</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> <span class="id" type="var">T</span> ∧ <span class="id" type="var">well_formed_ty</span> <span class="id" type="var">S</span>.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">S</span> <span class="id" type="var">T</span> <span class="id" type="var">Hsub</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hsub</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span>; <span class="id" type="tactic">try</span> (<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHsub1</span>; <span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHsub2</span>)...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;S_RcdPerm&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">split</span>... <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>5</sub></span>... <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">wf_rcd_lookup</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">i</span> <span class="id" type="var">T</span> <span class="id" type="var">Ti</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">Tlookup</span> <span class="id" type="var">i</span> <span class="id" type="var">T</span> = <span class="id" type="var">Some</span> <span class="id" type="var">Ti</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> <span class="id" type="var">Ti</span>.<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">i</span> <span class="id" type="var">T</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">T</span>; <span class="id" type="tactic">intros</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;RCons&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">Tlookup</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqb_string</span> <span class="id" type="var">i</span> <span class="id" type="var">s</span>)... <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>0</sub></span>; <span class="id" type="tactic">subst</span>... <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab415"></a><h3 class="section">Field Lookup</h3>

<div class="paragraph"> </div>

 The record matching lemmas get a little more complicated in the
    presence of subtyping, for two reasons.  First, record types no
    longer necessarily describe the exact structure of the
    corresponding terms.  And second, reasoning by induction on typing
    derivations becomes harder in general, because typing is no longer
    syntax directed. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">rcd_types_match</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">S</span> <span class="id" type="var">T</span> <span class="id" type="var">i</span> <span class="id" type="var">Ti</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">S</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">Tlookup</span> <span class="id" type="var">i</span> <span class="id" type="var">T</span> = <span class="id" type="var">Some</span> <span class="id" type="var">Ti</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">Si</span>, <span class="id" type="var">Tlookup</span> <span class="id" type="var">i</span> <span class="id" type="var">S</span> = <span class="id" type="var">Some</span> <span class="id" type="var">Si</span> ∧ <span class="id" type="var">subtype</span> <span class="id" type="var">Si</span> <span class="id" type="var">Ti</span>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> (<span class="id" type="tactic">eauto</span> <span class="id" type="keyword">using</span> <span class="id" type="var">wf_rcd_lookup</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">S</span> <span class="id" type="var">T</span> <span class="id" type="var">i</span> <span class="id" type="var">Ti</span> <span class="id" type="var">Hsub</span> <span class="id" type="var">Hget</span>. <span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">Ti</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hsub</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">Ti</span> <span class="id" type="var">Hget</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> <span class="id" type="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;S_Refl&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">Ti</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;S_Trans&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">IHHsub2</span> <span class="id" type="var">Ti</span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">Ui</span> <span class="id" type="var">Hui</span>]... <span class="id" type="tactic">destruct</span> <span class="id" type="var">Hui</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">IHHsub1</span> <span class="id" type="var">Ui</span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">Si</span> <span class="id" type="var">Hsi</span>]... <span class="id" type="tactic">destruct</span> <span class="id" type="var">Hsi</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">Si</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;S_RcdDepth&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rename</span> <span class="id" type="var">i<sub>0</sub></span> <span class="id" type="var">into</span> <span class="id" type="var">k</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">Tlookup</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">Tlookup</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hget</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqb_string</span> <span class="id" type="var">i</span> <span class="id" type="var">k</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;i&nbsp;=&nbsp;k&nbsp;--&nbsp;we're&nbsp;looking&nbsp;up&nbsp;the&nbsp;first&nbsp;field&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hget</span>. <span class="id" type="tactic">subst</span>. <span style='font-size:120%;'>&exist;</span><span class="id" type="var">S<sub>1</sub></span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;S_RcdPerm&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">Ti</span>. <span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;lookup&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">Tlookup</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">Tlookup</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hget</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqb_stringP</span> <span class="id" type="var">i</span> <span class="id" type="var">i<sub>1</sub></span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;i&nbsp;=&nbsp;i<sub>1</sub>&nbsp;--&nbsp;we're&nbsp;looking&nbsp;up&nbsp;the&nbsp;first&nbsp;field&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqb_stringP</span> <span class="id" type="var">i</span> <span class="id" type="var">i<sub>2</sub></span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;i&nbsp;=&nbsp;i<sub>2</sub>&nbsp;--&nbsp;contradictory&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;subtype&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>5</sub></span>. <span class="id" type="tactic">subst</span>... <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab416"></a><h4 class="section">Exercise: 3 stars, standard (rcd_types_match_informal)</h4>
 Write a careful informal proof of the <span class="inlinecode"><span class="id" type="var">rcd_types_match</span></span>
    lemma. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_rcd_types_match_informal</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab417"></a><h3 class="section">Inversion Lemmas</h3>

<div class="paragraph"> </div>

<a name="lab418"></a><h4 class="section">Exercise: 3 stars, standard, optional (sub_inversion_arrow)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">sub_inversion_arrow</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">U</span> <span class="id" type="var">V<sub>1</sub></span> <span class="id" type="var">V<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">U</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">V<sub>1</sub></span> <span class="id" type="var">V<sub>2</sub></span>) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">U<sub>1</sub></span> <span class="id" type="var">U<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">U</span>=(<span class="id" type="var">Arrow</span> <span class="id" type="var">U<sub>1</sub></span> <span class="id" type="var">U<sub>2</sub></span>)) ∧ (<span class="id" type="var">subtype</span> <span class="id" type="var">V<sub>1</sub></span> <span class="id" type="var">U<sub>1</sub></span>) ∧ (<span class="id" type="var">subtype</span> <span class="id" type="var">U<sub>2</sub></span> <span class="id" type="var">V<sub>2</sub></span>).<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">U</span> <span class="id" type="var">V<sub>1</sub></span> <span class="id" type="var">V<sub>2</sub></span> <span class="id" type="var">Hs</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">V<sub>1</sub></span> <span class="id" type="var">V<sub>2</sub></span>) <span class="id" type="keyword">as</span> <span class="id" type="var">V</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">V<sub>2</sub></span>. <span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">V<sub>1</sub></span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<br/>
</div>

<div class="doc">
<a name="lab419"></a><h1 class="section">Typing</h1>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">context</span> := <span class="id" type="var">partial_map</span> <span class="id" type="var">ty</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Reserved Notation</span> "Gamma '&#x22A2;' t '&#x2208;' T" (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">has_type</span> : <span class="id" type="var">context</span> → <span class="id" type="var">tm</span> → <span class="id" type="var">ty</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Var</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> = <span class="id" type="var">Some</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">var</span> <span class="id" type="var">x</span> &#x2208; <span class="id" type="var">T</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Abs</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">T<sub>11</sub></span> <span class="id" type="var">T<sub>12</sub></span> <span class="id" type="var">t<sub>12</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">well_formed_ty</span> <span class="id" type="var">T<sub>11</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">update</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">T<sub>11</sub></span> &#x22A2; <span class="id" type="var">t<sub>12</sub></span> &#x2208; <span class="id" type="var">T<sub>12</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">T<sub>11</sub></span> <span class="id" type="var">t<sub>12</sub></span> &#x2208; <span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>11</sub></span> <span class="id" type="var">T<sub>12</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_App</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span> <span class="id" type="var">Gamma</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t<sub>1</sub></span> &#x2208; <span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t<sub>2</sub></span> &#x2208; <span class="id" type="var">T<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> &#x2208; <span class="id" type="var">T<sub>2</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Proj</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">i</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span class="id" type="var">Ti</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Tlookup</span> <span class="id" type="var">i</span> <span class="id" type="var">T</span> = <span class="id" type="var">Some</span> <span class="id" type="var">Ti</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">rproj</span> <span class="id" type="var">t</span> <span class="id" type="var">i</span> &#x2208; <span class="id" type="var">Ti</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Subsumption&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_Sub</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">t</span> <span class="id" type="var">S</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">S</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">S</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Rules&nbsp;for&nbsp;record&nbsp;terms&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_RNil</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">rnil</span> &#x2208; <span class="id" type="var">RNil</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">T_RCons</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">i</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span class="id" type="var">tr</span> <span class="id" type="var">Tr</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">t</span> &#x2208; <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">tr</span> &#x2208; <span class="id" type="var">Tr</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">record_ty</span> <span class="id" type="var">Tr</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">record_tm</span> <span class="id" type="var">tr</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> &#x22A2; <span class="id" type="var">rcons</span> <span class="id" type="var">i</span> <span class="id" type="var">t</span> <span class="id" type="var">tr</span> &#x2208; <span class="id" type="var">RCons</span> <span class="id" type="var">i</span> <span class="id" type="var">T</span> <span class="id" type="var">Tr</span><br/>
<br/>
<span class="id" type="keyword">where</span> "Gamma '&#x22A2;' t '&#x2208;' T" := (<span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">has_type</span>.<br/>
</div>

<div class="doc">
<a name="lab420"></a><h2 class="section">Typing Examples</h2>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">Examples2</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">Examples</span>.<br/>
</div>

<div class="doc">
<a name="lab421"></a><h4 class="section">Exercise: 1 star, standard (typing_example_0)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Definition</span> <span class="id" type="var">trcd_kj</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">rcons</span> <span class="id" type="var">k</span> (<span class="id" type="var">abs</span> <span class="id" type="var">z</span> <span class="id" type="var">A</span> (<span class="id" type="var">var</span> <span class="id" type="var">z</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">rcons</span> <span class="id" type="var">j</span> (<span class="id" type="var">abs</span> <span class="id" type="var">z</span> <span class="id" type="var">B</span> (<span class="id" type="var">var</span> <span class="id" type="var">z</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">rnil</span>)).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">typing_example_0</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">rcons</span> <span class="id" type="var">k</span> (<span class="id" type="var">abs</span> <span class="id" type="var">z</span> <span class="id" type="var">A</span> (<span class="id" type="var">var</span> <span class="id" type="var">z</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">rcons</span> <span class="id" type="var">j</span> (<span class="id" type="var">abs</span> <span class="id" type="var">z</span> <span class="id" type="var">B</span> (<span class="id" type="var">var</span> <span class="id" type="var">z</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">rnil</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">TRcd_kj</span>.<br/>
<span class="comment">(*&nbsp;empty&nbsp;&#x22A2;&nbsp;{k=(\z:A.z),&nbsp;j=(\z:B.z)}&nbsp;:&nbsp;{k:A<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>A,j:B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B}&nbsp;*)</span><br/>
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<br/>
</div>

<div class="doc">
<a name="lab422"></a><h4 class="section">Exercise: 2 stars, standard (typing_example_1)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Example</span> <span class="id" type="var">typing_example_1</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">app</span> (<span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">TRcd_j</span> (<span class="id" type="var">rproj</span> (<span class="id" type="var">var</span> <span class="id" type="var">x</span>) <span class="id" type="var">j</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">trcd_kj</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">Arrow</span> <span class="id" type="var">B</span> <span class="id" type="var">B</span>).<br/>
<span class="comment">(*&nbsp;empty&nbsp;&#x22A2;&nbsp;(\x:{k:A<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>A,j:B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B}.&nbsp;x.j)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;{k=(\z:A.z),&nbsp;j=(\z:B.z)}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:&nbsp;B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B&nbsp;*)</span><br/>
<div class="togglescript" id="proofcontrol6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')"><span class="show"></span></div>
<div class="proofscript" id="proof6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<br/>
</div>

<div class="doc">
<a name="lab423"></a><h4 class="section">Exercise: 2 stars, standard, optional (typing_example_2)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Example</span> <span class="id" type="var">typing_example_2</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">app</span> (<span class="id" type="var">abs</span> <span class="id" type="var">z</span> (<span class="id" type="var">Arrow</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">C</span> <span class="id" type="var">C</span>) <span class="id" type="var">TRcd_j</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">rproj</span> (<span class="id" type="var">app</span> (<span class="id" type="var">var</span> <span class="id" type="var">z</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">C</span> (<span class="id" type="var">var</span> <span class="id" type="var">x</span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">j</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">abs</span> <span class="id" type="var">z</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">C</span> <span class="id" type="var">C</span>) <span class="id" type="var">trcd_kj</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">Arrow</span> <span class="id" type="var">B</span> <span class="id" type="var">B</span>).<br/>
<span class="comment">(*&nbsp;empty&nbsp;&#x22A2;&nbsp;(\z:(C<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>C)<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>{j:B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B}.&nbsp;(z&nbsp;(\x:C.x)).j)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(\z:C<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>C.&nbsp;{k=(\z:A.z),&nbsp;j=(\z:B.z)})<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:&nbsp;B<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>B&nbsp;*)</span><br/>
<div class="togglescript" id="proofcontrol7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')"><span class="show"></span></div>
<div class="proofscript" id="proof7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<br/>
<span class="id" type="keyword">End</span> <span class="id" type="var">Examples2</span>.<br/>
</div>

<div class="doc">
<a name="lab424"></a><h2 class="section">Properties of Typing</h2>

<div class="paragraph"> </div>

<a name="lab425"></a><h3 class="section">Well-Formedness</h3>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">has_type__wf</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> → <span class="id" type="var">well_formed_ty</span> <span class="id" type="var">T</span>.<br/>
<div class="togglescript" id="proofcontrol8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')"><span class="show"></span></div>
<div class="proofscript" id="proof8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span class="id" type="var">Htyp</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Htyp</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">IHHtyp1</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Proj&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">wf_rcd_lookup</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Sub&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">subtype__wf</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">H</span>...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">step_preserves_record_tm</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">tr</span> <span class="id" type="var">tr'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">record_tm</span> <span class="id" type="var">tr</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">tr</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">tr'</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">record_tm</span> <span class="id" type="var">tr'</span>.<br/>
<div class="togglescript" id="proofcontrol9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')"><span class="show"></span></div>
<div class="proofscript" id="proof9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">tr</span> <span class="id" type="var">tr'</span> <span class="id" type="var">Hrt</span> <span class="id" type="var">Hstp</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hrt</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">Hstp</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">eauto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab426"></a><h3 class="section">Field Lookup</h3>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">lookup_field_in_value</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">v</span> <span class="id" type="var">T</span> <span class="id" type="var">i</span> <span class="id" type="var">Ti</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">v</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">v</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">Tlookup</span> <span class="id" type="var">i</span> <span class="id" type="var">T</span> = <span class="id" type="var">Some</span> <span class="id" type="var">Ti</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">vi</span>, <span class="id" type="var">tlookup</span> <span class="id" type="var">i</span> <span class="id" type="var">v</span> = <span class="id" type="var">Some</span> <span class="id" type="var">vi</span> ∧ <span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">vi</span> <span class="id" type="var">Ti</span>.<br/>
<div class="togglescript" id="proofcontrol10" onclick="toggleDisplay('proof10');toggleDisplay('proofcontrol10')"><span class="show"></span></div>
<div class="proofscript" id="proof10" onclick="toggleDisplay('proof10');toggleDisplay('proofcontrol10')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> <span class="id" type="var">empty</span> <span class="id" type="keyword">as</span> <span class="id" type="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span class="id" type="var">i</span> <span class="id" type="var">Ti</span> <span class="id" type="var">Hval</span> <span class="id" type="var">Htyp</span>. <span class="id" type="var">revert</span> <span class="id" type="var">Ti</span> <span class="id" type="var">HeqGamma</span> <span class="id" type="var">Hval</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Htyp</span>; <span class="id" type="tactic">intros</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Sub&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">rcd_types_match</span> <span class="id" type="var">S</span>) <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>0</sub></span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">H<sub>0</sub></span> <span class="id" type="keyword">as</span> [<span class="id" type="var">Si</span> [<span class="id" type="var">HgetSi</span> <span class="id" type="var">Hsub</span>]].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">IHHtyp</span> <span class="id" type="var">Si</span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">vi</span> [<span class="id" type="var">Hget</span> <span class="id" type="var">Htyvi</span>]]...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_RCons&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>0</sub></span>. <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqb_string</span> <span class="id" type="var">i</span> <span class="id" type="var">i<sub>0</sub></span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;i&nbsp;is&nbsp;first&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>1</sub></span>. <span class="id" type="tactic">subst</span>. <span style='font-size:120%;'>&exist;</span><span class="id" type="var">t</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;i&nbsp;in&nbsp;tail&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">IHHtyp2</span> <span class="id" type="var">Ti</span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">vi</span> [<span class="id" type="var">get</span> <span class="id" type="var">Htyvi</span>]]...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hval</span>... <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab427"></a><h3 class="section">Progress</h3>

<div class="paragraph"> </div>

<a name="lab428"></a><h4 class="section">Exercise: 3 stars, standard (canonical_forms_of_arrow_types)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">canonical_forms_of_arrow_types</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">s</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">s</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">s</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s</span> = <span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span>.<br/>
<div class="togglescript" id="proofcontrol11" onclick="toggleDisplay('proof11');toggleDisplay('proofcontrol11')"><span class="show"></span></div>
<div class="proofscript" id="proof11" onclick="toggleDisplay('proof11');toggleDisplay('proofcontrol11')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="tactic">progress</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">t</span> ∨ <span style='font-size:120%;'>&exist;</span><span class="id" type="var">t'</span>, <span class="id" type="var">t</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t'</span>.<br/>
<div class="togglescript" id="proofcontrol12" onclick="toggleDisplay('proof12');toggleDisplay('proofcontrol12')"><span class="show"></span></div>
<div class="proofscript" id="proof12" onclick="toggleDisplay('proof12');toggleDisplay('proofcontrol12')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span class="id" type="var">Ht</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> <span class="id" type="var">empty</span> <span class="id" type="keyword">as</span> <span class="id" type="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">revert</span> <span class="id" type="var">HeqGamma</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Ht</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">HeqGamma</span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Var&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHt1</span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHt2</span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;t<sub>2</sub>&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">canonical_forms_of_arrow_types</span> <span class="id" type="var">empty</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [<span class="id" type="var">x</span> [<span class="id" type="var">S<sub>1</sub></span> [<span class="id" type="var">t<sub>12</sub></span> <span class="id" type="var">Heqt1</span>]]]...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span>. <span style='font-size:120%;'>&exist;</span>([<span class="id" type="var">x</span>:=<span class="id" type="var">t<sub>2</sub></span>]<span class="id" type="var">t<sub>12</sub></span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;t<sub>2</sub>&nbsp;steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">H<sub>0</sub></span> <span class="id" type="keyword">as</span> [<span class="id" type="var">t<sub>2</sub>'</span> <span class="id" type="var">Hstp</span>]. <span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub>'</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">H</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">Hstp</span>]. <span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">t<sub>2</sub></span>)...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Proj&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHt</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;rcd&nbsp;is&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">lookup_field_in_value</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span class="id" type="var">i</span> <span class="id" type="var">Ti</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [<span class="id" type="var">t'</span> [<span class="id" type="var">Hget</span> <span class="id" type="var">Ht'</span>]]...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;rcd_steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">H<sub>0</sub></span> <span class="id" type="keyword">as</span> [<span class="id" type="var">t'</span> <span class="id" type="var">Hstp</span>]. <span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">rproj</span> <span class="id" type="var">t'</span> <span class="id" type="var">i</span>)...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_RCons&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHt1</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;head&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHt2</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;tail&nbsp;steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">H<sub>2</sub></span> <span class="id" type="keyword">as</span> [<span class="id" type="var">tr'</span> <span class="id" type="var">Hstp</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">rcons</span> <span class="id" type="var">i</span> <span class="id" type="var">t</span> <span class="id" type="var">tr'</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;head&nbsp;steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">H<sub>1</sub></span> <span class="id" type="keyword">as</span> [<span class="id" type="var">t'</span> <span class="id" type="var">Hstp</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">rcons</span> <span class="id" type="var">i</span> <span class="id" type="var">t'</span> <span class="id" type="var">tr</span>)... <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<i>Theorem</i> : For any term <span class="inlinecode"><span class="id" type="var">t</span></span> and type <span class="inlinecode"><span class="id" type="var">T</span></span>, if <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">T</span></span>
    then <span class="inlinecode"><span class="id" type="var">t</span></span> is a value or <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t'</span></span> for some term <span class="inlinecode"><span class="id" type="var">t'</span></span>.

<div class="paragraph"> </div>

    <i>Proof</i>: Let <span class="inlinecode"><span class="id" type="var">t</span></span> and <span class="inlinecode"><span class="id" type="var">T</span></span> be given such that <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.  We
    proceed by induction on the given typing derivation.

<div class="paragraph"> </div>

<ul class="doclist">
<li> The cases where the last step in the typing derivation is
        <span class="inlinecode"><span class="id" type="var">T_Abs</span></span> or <span class="inlinecode"><span class="id" type="var">T_RNil</span></span> are immediate because abstractions and
        <span class="inlinecode">{}</span> are always values.  The case for <span class="inlinecode"><span class="id" type="var">T_Var</span></span> is vacuous
        because variables cannot be typed in the empty context.

<div class="paragraph"> </div>


</li>
<li> If the last step in the typing derivation is by <span class="inlinecode"><span class="id" type="var">T_App</span></span>, then
        there are terms <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> and types <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span> such that <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span>
        <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>, <span class="inlinecode"><span class="id" type="var">T</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span>, <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span> and <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode">:</span>
        <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span>.

<div class="paragraph"> </div>

        The induction hypotheses for these typing derivations yield
        that <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> is a value or steps, and that <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> is a value or
        steps.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Suppose <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span> for some term <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span>.  Then <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span>
          <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> by <span class="inlinecode"><span class="id" type="var">ST_App1</span></span>.

<div class="paragraph"> </div>


</li>
<li> Otherwise <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> is a value.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Suppose <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub>'</span></span> for some term <span class="inlinecode"><span class="id" type="var">t<sub>2</sub>'</span></span>.  Then <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span>
            <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub>'</span></span> by rule <span class="inlinecode"><span class="id" type="var">ST_App2</span></span> because <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> is a value.

<div class="paragraph"> </div>


</li>
<li> Otherwise, <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> is a value.  By Lemma
            <span class="inlinecode"><span class="id" type="var">canonical_forms_for_arrow_types</span></span>, <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode">\<span class="id" type="var">x</span>:<span class="id" type="var">S<sub>1</sub>.s2</span></span> for
            some <span class="inlinecode"><span class="id" type="var">x</span></span>, <span class="inlinecode"><span class="id" type="var">S<sub>1</sub></span></span>, and <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span>.  But then <span class="inlinecode">(\<span class="id" type="var">x</span>:<span class="id" type="var">S<sub>1</sub>.s2</span>)</span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span>
            <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">t<sub>2</sub></span>]<span class="id" type="var">s<sub>2</sub></span></span> by <span class="inlinecode"><span class="id" type="var">ST_AppAbs</span></span>, since <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> is a value.

<div class="paragraph"> </div>


</li>
</ul>

</li>
</ul>

</li>
<li> If the last step of the derivation is by <span class="inlinecode"><span class="id" type="var">T_Proj</span></span>, then there
        are a term <span class="inlinecode"><span class="id" type="var">tr</span></span>, a type <span class="inlinecode"><span class="id" type="var">Tr</span></span>, and a label <span class="inlinecode"><span class="id" type="var">i</span></span> such that <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span>
        <span class="inlinecode"><span class="id" type="var">tr.i</span></span>, <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">tr</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">Tr</span></span>, and <span class="inlinecode"><span class="id" type="var">Tlookup</span></span> <span class="inlinecode"><span class="id" type="var">i</span></span> <span class="inlinecode"><span class="id" type="var">Tr</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">Some</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span>.

<div class="paragraph"> </div>

        By the IH, either <span class="inlinecode"><span class="id" type="var">tr</span></span> is a value or it steps.  If <span class="inlinecode"><span class="id" type="var">tr</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span>
        <span class="inlinecode"><span class="id" type="var">tr'</span></span> for some term <span class="inlinecode"><span class="id" type="var">tr'</span></span>, then <span class="inlinecode"><span class="id" type="var">tr.i</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">tr'.i</span></span> by rule
        <span class="inlinecode"><span class="id" type="var">ST_Proj1</span></span>.

<div class="paragraph"> </div>

        If <span class="inlinecode"><span class="id" type="var">tr</span></span> is a value, then Lemma <span class="inlinecode"><span class="id" type="var">lookup_field_in_value</span></span> yields
        that there is a term <span class="inlinecode"><span class="id" type="var">ti</span></span> such that <span class="inlinecode"><span class="id" type="var">tlookup</span></span> <span class="inlinecode"><span class="id" type="var">i</span></span> <span class="inlinecode"><span class="id" type="var">tr</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">Some</span></span> <span class="inlinecode"><span class="id" type="var">ti</span></span>.
        It follows that <span class="inlinecode"><span class="id" type="var">tr.i</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">ti</span></span> by rule <span class="inlinecode"><span class="id" type="var">ST_ProjRcd</span></span>.

<div class="paragraph"> </div>


</li>
<li> If the final step of the derivation is by <span class="inlinecode"><span class="id" type="var">T_Sub</span></span>, then there
        is a type <span class="inlinecode"><span class="id" type="var">S</span></span> such that <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">T</span></span> and <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">S</span></span>.  The
        desired result is exactly the induction hypothesis for the
        typing subderivation.

<div class="paragraph"> </div>


</li>
<li> If the final step of the derivation is by <span class="inlinecode"><span class="id" type="var">T_RCons</span></span>, then
        there exist some terms <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">tr</span></span>, types <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">Tr</span></span> and a label
        <span class="inlinecode"><span class="id" type="var">t</span></span> such that <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode">{<span class="id" type="var">i</span>=<span class="id" type="var">t<sub>1</sub></span>,</span> <span class="inlinecode"><span class="id" type="var">tr</span>}</span>, <span class="inlinecode"><span class="id" type="var">T</span></span> <span class="inlinecode">=</span> <span class="inlinecode">{<span class="id" type="var">i</span>:<span class="id" type="var">T<sub>1</sub></span>,</span> <span class="inlinecode"><span class="id" type="var">Tr</span>}</span>, <span class="inlinecode"><span class="id" type="var">record_ty</span></span>
        <span class="inlinecode"><span class="id" type="var">tr</span></span>, <span class="inlinecode"><span class="id" type="var">record_tm</span></span> <span class="inlinecode"><span class="id" type="var">Tr</span></span>, <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">tr</span></span> <span class="inlinecode">:</span>
        <span class="inlinecode"><span class="id" type="var">Tr</span></span>.

<div class="paragraph"> </div>

        The induction hypotheses for these typing derivations yield
        that <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> is a value or steps, and that <span class="inlinecode"><span class="id" type="var">tr</span></span> is a value or
        steps.  We consider each case:

<div class="paragraph"> </div>

<ul class="doclist">
<li> Suppose <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span> for some term <span class="inlinecode"><span class="id" type="var">t<sub>1</sub>'</span></span>.  Then <span class="inlinecode">{<span class="id" type="var">i</span>=<span class="id" type="var">t<sub>1</sub></span>,</span> <span class="inlinecode"><span class="id" type="var">tr</span>}</span>
          <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode">{<span class="id" type="var">i</span>=<span class="id" type="var">t<sub>1</sub>'</span>,</span> <span class="inlinecode"><span class="id" type="var">tr</span>}</span> by rule <span class="inlinecode"><span class="id" type="var">ST_Rcd_Head</span></span>.

<div class="paragraph"> </div>


</li>
<li> Otherwise <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> is a value.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Suppose <span class="inlinecode"><span class="id" type="var">tr</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">tr'</span></span> for some term <span class="inlinecode"><span class="id" type="var">tr'</span></span>.  Then <span class="inlinecode">{<span class="id" type="var">i</span>=<span class="id" type="var">t<sub>1</sub></span>,</span>
            <span class="inlinecode"><span class="id" type="var">tr</span>}</span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode">{<span class="id" type="var">i</span>=<span class="id" type="var">t<sub>1</sub></span>,</span> <span class="inlinecode"><span class="id" type="var">tr'</span>}</span> by rule <span class="inlinecode"><span class="id" type="var">ST_Rcd_Tail</span></span>, since <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> is
            a value.

<div class="paragraph"> </div>


</li>
<li> Otherwise, <span class="inlinecode"><span class="id" type="var">tr</span></span> is also a value.  So, <span class="inlinecode">{<span class="id" type="var">i</span>=<span class="id" type="var">t<sub>1</sub></span>,</span> <span class="inlinecode"><span class="id" type="var">tr</span>}</span> is a
            value by <span class="inlinecode"><span class="id" type="var">v_rcons</span></span>. 
</li>
</ul>

</li>
</ul>

</li>
</ul>

</div>

<div class="doc">
<a name="lab429"></a><h3 class="section">Inversion Lemmas</h3>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">typing_inversion_var</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> (<span class="id" type="var">var</span> <span class="id" type="var">x</span>) <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">S</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> = <span class="id" type="var">Some</span> <span class="id" type="var">S</span> ∧ <span class="id" type="var">subtype</span> <span class="id" type="var">S</span> <span class="id" type="var">T</span>.<br/>
<div class="togglescript" id="proofcontrol13" onclick="toggleDisplay('proof13');toggleDisplay('proofcontrol13')"><span class="show"></span></div>
<div class="proofscript" id="proof13" onclick="toggleDisplay('proof13');toggleDisplay('proofcontrol13')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">T</span> <span class="id" type="var">Hty</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">var</span> <span class="id" type="var">x</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">t</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hty</span>; <span class="id" type="tactic">intros</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqt</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Var&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">T</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Sub&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHty</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">U</span> [<span class="id" type="var">Hctx</span> <span class="id" type="var">HsubU</span>]]... <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">typing_inversion_app</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> (<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) <span class="id" type="var">T<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">T<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">t<sub>1</sub></span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>) ∧<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">T<sub>1</sub></span>.<br/>
<div class="togglescript" id="proofcontrol14" onclick="toggleDisplay('proof14');toggleDisplay('proofcontrol14')"><span class="show"></span></div>
<div class="proofscript" id="proof14" onclick="toggleDisplay('proof14');toggleDisplay('proofcontrol14')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">T<sub>2</sub></span> <span class="id" type="var">Hty</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) <span class="id" type="keyword">as</span> <span class="id" type="var">t</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hty</span>; <span class="id" type="tactic">intros</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqt</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">T<sub>1</sub></span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Sub&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHty</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">U<sub>1</sub></span> [<span class="id" type="var">Hty1</span> <span class="id" type="var">Hty2</span>]]...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">Hwf</span> := <span class="id" type="var">has_type__wf</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">Hty2</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">U<sub>1</sub></span>... <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">typing_inversion_abs</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> (<span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&exist;</span><span class="id" type="var">S<sub>2</sub></span>, <span class="id" type="var">subtype</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">S<sub>2</sub></span>) <span class="id" type="var">T</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;∧ <span class="id" type="var">has_type</span> (<span class="id" type="var">update</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span>) <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">S<sub>2</sub></span>).<br/>
<div class="togglescript" id="proofcontrol15" onclick="toggleDisplay('proof15');toggleDisplay('proofcontrol15')"><span class="show"></span></div>
<div class="proofscript" id="proof15" onclick="toggleDisplay('proof15');toggleDisplay('proofcontrol15')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">T</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>) <span class="id" type="keyword">as</span> <span class="id" type="var">t</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">H</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqt</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">intros</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Abs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">Hwf</span> := <span class="id" type="var">has_type__wf</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">H<sub>0</sub></span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">T<sub>12</sub></span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Sub&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHhas_type</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">S<sub>2</sub></span> [<span class="id" type="var">Hsub</span> <span class="id" type="var">Hty</span>]]...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">typing_inversion_proj</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">i</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">Ti</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> (<span class="id" type="var">rproj</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">i</span>) <span class="id" type="var">Ti</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">T</span> <span class="id" type="var">Si</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Tlookup</span> <span class="id" type="var">i</span> <span class="id" type="var">T</span> = <span class="id" type="var">Some</span> <span class="id" type="var">Si</span> ∧ <span class="id" type="var">subtype</span> <span class="id" type="var">Si</span> <span class="id" type="var">Ti</span> ∧ <span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">T</span>.<br/>
<div class="togglescript" id="proofcontrol16" onclick="toggleDisplay('proof16');toggleDisplay('proofcontrol16')"><span class="show"></span></div>
<div class="proofscript" id="proof16" onclick="toggleDisplay('proof16');toggleDisplay('proofcontrol16')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">i</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">Ti</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">rproj</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">i</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">t</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">H</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqt</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">intros</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Proj&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">well_formed_ty</span> <span class="id" type="var">Ti</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">Hwf</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="comment">(*&nbsp;pf&nbsp;of&nbsp;assertion&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">wf_rcd_lookup</span> <span class="id" type="var">i</span> <span class="id" type="var">T</span> <span class="id" type="var">Ti</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">has_type__wf</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>... }<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">T</span>, <span class="id" type="var">Ti</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Sub&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHhas_type</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">U</span> [<span class="id" type="var">Ui</span> [<span class="id" type="var">Hget</span> [<span class="id" type="var">Hsub</span> <span class="id" type="var">Hty</span>]]]]...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">U</span>, <span class="id" type="var">Ui</span>... <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">typing_inversion_rcons</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">i</span> <span class="id" type="var">ti</span> <span class="id" type="var">tr</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> (<span class="id" type="var">rcons</span> <span class="id" type="var">i</span> <span class="id" type="var">ti</span> <span class="id" type="var">tr</span>) <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">Si</span> <span class="id" type="var">Sr</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">subtype</span> (<span class="id" type="var">RCons</span> <span class="id" type="var">i</span> <span class="id" type="var">Si</span> <span class="id" type="var">Sr</span>) <span class="id" type="var">T</span> ∧ <span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">ti</span> <span class="id" type="var">Si</span> ∧<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">record_tm</span> <span class="id" type="var">tr</span> ∧ <span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">tr</span> <span class="id" type="var">Sr</span>.<br/>
<div class="togglescript" id="proofcontrol17" onclick="toggleDisplay('proof17');toggleDisplay('proofcontrol17')"><span class="show"></span></div>
<div class="proofscript" id="proof17" onclick="toggleDisplay('proof17');toggleDisplay('proofcontrol17')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">i</span> <span class="id" type="var">ti</span> <span class="id" type="var">tr</span> <span class="id" type="var">T</span> <span class="id" type="var">Hty</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">rcons</span> <span class="id" type="var">i</span> <span class="id" type="var">ti</span> <span class="id" type="var">tr</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">t</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hty</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqt</span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Sub&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHHty</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">H<sub>0</sub></span> <span class="id" type="keyword">as</span> [<span class="id" type="var">Ri</span> [<span class="id" type="var">Rr</span> [<span class="id" type="var">HsubRS</span> [<span class="id" type="var">HtypRi</span> <span class="id" type="var">HtypRr</span>]]]].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">Ri</span>, <span class="id" type="var">Rr</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_RCons&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">well_formed_ty</span> (<span class="id" type="var">RCons</span> <span class="id" type="var">i</span> <span class="id" type="var">T</span> <span class="id" type="var">Tr</span>)) <span class="id" type="keyword">as</span> <span class="id" type="var">Hwf</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="comment">(*&nbsp;pf&nbsp;of&nbsp;assertion&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">has_type__wf</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hty1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">has_type__wf</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hty2</span>... }<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">T</span>, <span class="id" type="var">Tr</span>... <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">abs_arrow</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> (<span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span>) (<span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">S<sub>1</sub></span><br/>
&nbsp;&nbsp;∧ <span class="id" type="var">has_type</span> (<span class="id" type="var">update</span> <span class="id" type="var">empty</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span>) <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">T<sub>2</sub></span>.<br/>
<div class="togglescript" id="proofcontrol18" onclick="toggleDisplay('proof18');toggleDisplay('proofcontrol18')"><span class="show"></span></div>
<div class="proofscript" id="proof18" onclick="toggleDisplay('proof18');toggleDisplay('proofcontrol18')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span> <span class="id" type="var">Hty</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">typing_inversion_abs</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hty</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">Hty</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">S<sub>2</sub></span> [<span class="id" type="var">Hsub</span> <span class="id" type="var">Hty</span>]].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">sub_inversion_arrow</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hsub</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">Hsub</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">U<sub>1</sub></span> [<span class="id" type="var">U<sub>2</sub></span> [<span class="id" type="var">Heq</span> [<span class="id" type="var">Hsub1</span> <span class="id" type="var">Hsub2</span>]]]].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heq</span>; <span class="id" type="tactic">subst</span>... <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab430"></a><h3 class="section">Context Invariance</h3>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">appears_free_in</span> : <span class="id" type="var">string</span> → <span class="id" type="var">tm</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_var</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">var</span> <span class="id" type="var">x</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_app1</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> → <span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_app2</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t<sub>2</sub></span> → <span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_abs</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="var">T<sub>11</sub></span> <span class="id" type="var">t<sub>12</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">y</span> ≠ <span class="id" type="var">x</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t<sub>12</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">abs</span> <span class="id" type="var">y</span> <span class="id" type="var">T<sub>11</sub></span> <span class="id" type="var">t<sub>12</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_proj</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t</span> <span class="id" type="var">i</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">rproj</span> <span class="id" type="var">t</span> <span class="id" type="var">i</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_rhead</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">i</span> <span class="id" type="var">t</span> <span class="id" type="var">tr</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">rcons</span> <span class="id" type="var">i</span> <span class="id" type="var">t</span> <span class="id" type="var">tr</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">afi_rtail</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">i</span> <span class="id" type="var">t</span> <span class="id" type="var">tr</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">tr</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> (<span class="id" type="var">rcons</span> <span class="id" type="var">i</span> <span class="id" type="var">t</span> <span class="id" type="var">tr</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">appears_free_in</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">context_invariance</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">Gamma'</span> <span class="id" type="var">t</span> <span class="id" type="var">S</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">t</span> <span class="id" type="var">S</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>, <span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t</span> → <span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> = <span class="id" type="var">Gamma'</span> <span class="id" type="var">x</span>)  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">Gamma'</span> <span class="id" type="var">t</span> <span class="id" type="var">S</span>.<br/>
<div class="togglescript" id="proofcontrol19" onclick="toggleDisplay('proof19');toggleDisplay('proofcontrol19')"><span class="show"></span></div>
<div class="proofscript" id="proof19" onclick="toggleDisplay('proof19');toggleDisplay('proofcontrol19')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">Gamma'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">H</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma'</span> <span class="id" type="var">Heqv</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Var&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_Var</span>... <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">Heqv</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Abs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_Abs</span>... <span class="id" type="tactic">apply</span> <span class="id" type="var">IHhas_type</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">x<sub>0</sub></span> <span class="id" type="var">Hafi</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">update</span>, <span class="id" type="var">t_update</span>. <span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqb_stringP</span> <span class="id" type="var">x</span> <span class="id" type="var">x<sub>0</sub></span>)...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_App</span> <span class="id" type="keyword">with</span> <span class="id" type="var">T<sub>1</sub></span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_RCons&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_RCons</span>... <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">free_in_context</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span class="id" type="var">Gamma</span>,<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">appears_free_in</span> <span class="id" type="var">x</span> <span class="id" type="var">t</span> →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">T'</span>, <span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> = <span class="id" type="var">Some</span> <span class="id" type="var">T'</span>.<br/>
<div class="togglescript" id="proofcontrol20" onclick="toggleDisplay('proof20');toggleDisplay('proofcontrol20')"><span class="show"></span></div>
<div class="proofscript" id="proof20" onclick="toggleDisplay('proof20');toggleDisplay('proofcontrol20')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">Hafi</span> <span class="id" type="var">Htyp</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Htyp</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">Hafi</span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Abs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">IHHtyp</span> <span class="id" type="var">H<sub>5</sub></span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">T</span> <span class="id" type="var">Hctx</span>]. <span style='font-size:120%;'>&exist;</span><span class="id" type="var">T</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">update</span>, <span class="id" type="var">t_update</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hctx</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">false_eqb_string</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hctx</span>... <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab431"></a><h3 class="section">Preservation</h3>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">substitution_preserves_typing</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">U</span> <span class="id" type="var">v</span> <span class="id" type="var">t</span> <span class="id" type="var">S</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">has_type</span> (<span class="id" type="var">update</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">U</span>) <span class="id" type="var">t</span> <span class="id" type="var">S</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">v</span> <span class="id" type="var">U</span>   →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">Gamma</span> ([<span class="id" type="var">x</span>:=<span class="id" type="var">v</span>]<span class="id" type="var">t</span>) <span class="id" type="var">S</span>.<br/>
<div class="togglescript" id="proofcontrol21" onclick="toggleDisplay('proof21');toggleDisplay('proofcontrol21')"><span class="show"></span></div>
<div class="proofscript" id="proof21" onclick="toggleDisplay('proof21');toggleDisplay('proofcontrol21')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Gamma</span> <span class="id" type="var">x</span> <span class="id" type="var">U</span> <span class="id" type="var">v</span> <span class="id" type="var">t</span> <span class="id" type="var">S</span> <span class="id" type="var">Htypt</span> <span class="id" type="var">Htypv</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">S</span>. <span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">t</span>; <span class="id" type="tactic">intros</span>; <span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;var&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rename</span> <span class="id" type="var">s</span> <span class="id" type="var">into</span> <span class="id" type="var">y</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">typing_inversion_var</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">Htypt</span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">T</span> [<span class="id" type="var">Hctx</span> <span class="id" type="var">Hsub</span>]].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">update</span>, <span class="id" type="var">t_update</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hctx</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqb_stringP</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;x=y&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hctx</span>; <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">clear</span> <span class="id" type="var">Hctx</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">context_invariance</span> <span class="id" type="keyword">with</span> <span class="id" type="var">empty</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">Hcontra</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">free_in_context</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">S</span> <span class="id" type="var">empty</span> <span class="id" type="var">Hcontra</span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">T'</span> <span class="id" type="var">HT'</span>]...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HT'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;x&lt;&gt;y&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">subtype__wf</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">Hsub</span>)...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;app&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">typing_inversion_app</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">Htypt</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [<span class="id" type="var">T<sub>1</sub></span> [<span class="id" type="var">Htypt1</span> <span class="id" type="var">Htypt2</span>]].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">T_App</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;abs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rename</span> <span class="id" type="var">s</span> <span class="id" type="var">into</span> <span class="id" type="var">y</span>. <span class="id" type="tactic">rename</span> <span class="id" type="var">t</span> <span class="id" type="var">into</span> <span class="id" type="var">T<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">typing_inversion_abs</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">Htypt</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [<span class="id" type="var">T<sub>2</sub></span> [<span class="id" type="var">Hsub</span> <span class="id" type="var">Htypt2</span>]].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">subtype__wf</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">Hsub</span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">Hwf1</span> <span class="id" type="var">Hwf2</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hwf2</span>. <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_Sub</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>)... <span class="id" type="tactic">apply</span> <span class="id" type="var">T_Abs</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqb_stringP</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;x=y&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">context_invariance</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">Hafi</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">update</span>, <span class="id" type="var">t_update</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqb_string</span> <span class="id" type="var">y</span> <span class="id" type="var">x</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;x&lt;&gt;y&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHt</span>. <span class="id" type="tactic">eapply</span> <span class="id" type="var">context_invariance</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">z</span> <span class="id" type="var">Hafi</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">update</span>, <span class="id" type="var">t_update</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqb_stringP</span> <span class="id" type="var">y</span> <span class="id" type="var">z</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">false_eqb_string</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;rproj&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">typing_inversion_proj</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">Htypt</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [<span class="id" type="var">T</span> [<span class="id" type="var">Ti</span> [<span class="id" type="var">Hget</span> [<span class="id" type="var">Hsub</span> <span class="id" type="var">Htypt1</span>]]]]...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;rnil&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">context_invariance</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">y</span> <span class="id" type="var">Hcontra</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">Hcontra</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;rcons&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">typing_inversion_rcons</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">Htypt</span>) <span class="id" type="keyword">as</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="var">Ti</span> [<span class="id" type="var">Tr</span> [<span class="id" type="var">Hsub</span> [<span class="id" type="var">HtypTi</span> [<span class="id" type="var">Hrcdt2</span> <span class="id" type="var">HtypTr</span>]]]]].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_Sub</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">RCons</span> <span class="id" type="var">s</span> <span class="id" type="var">Ti</span> <span class="id" type="var">Tr</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">T_RCons</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;record_ty&nbsp;Tr&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">subtype__wf</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hsub</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">Hsub</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>0</sub></span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;record_tm&nbsp;(<span class="inlinecode"><span class="id" type="var">x</span>:=<span class="id" type="var">v</span></span>t<sub>2</sub>)&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hrcdt2</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">simpl</span>... <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">preservation</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t'</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span>.<br/>
<div class="togglescript" id="proofcontrol22" onclick="toggleDisplay('proof22');toggleDisplay('proofcontrol22')"><span class="show"></span></div>
<div class="proofscript" id="proof22" onclick="toggleDisplay('proof22');toggleDisplay('proofcontrol22')">
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span> <span class="id" type="var">HT</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> <span class="id" type="var">empty</span> <span class="id" type="keyword">as</span> <span class="id" type="var">Gamma</span>. <span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">HeqGamma</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">t'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">HT</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t'</span> <span class="id" type="var">HeqGamma</span> <span class="id" type="var">HE</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">HE</span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HE</span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;ST_AppAbs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">abs_arrow</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">HT<sub>1</sub></span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">HA<sub>1</sub></span> <span class="id" type="var">HA<sub>2</sub></span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">substitution_preserves_typing</span> <span class="id" type="keyword">with</span> <span class="id" type="var">T</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Proj&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">lookup_field_in_value</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span> <span class="id" type="var">H<sub>2</sub></span> <span class="id" type="var">HT</span> <span class="id" type="var">H</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [<span class="id" type="var">vi</span> [<span class="id" type="var">Hget</span> <span class="id" type="var">Hty</span>]].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H<sub>4</sub></span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hget</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">Hget</span>. <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_RCons&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eauto</span> <span class="id" type="keyword">using</span> <span class="id" type="var">step_preserves_record_tm</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<i>Theorem</i>: If <span class="inlinecode"><span class="id" type="var">t</span></span>, <span class="inlinecode"><span class="id" type="var">t'</span></span> are terms and <span class="inlinecode"><span class="id" type="var">T</span></span> is a type such that
     <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">T</span></span> and <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">t'</span></span>, then <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.

<div class="paragraph"> </div>

    <i>Proof</i>: Let <span class="inlinecode"><span class="id" type="var">t</span></span> and <span class="inlinecode"><span class="id" type="var">T</span></span> be given such that <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.  We go
     by induction on the structure of this typing derivation, leaving
     <span class="inlinecode"><span class="id" type="var">t'</span></span> general.  Cases <span class="inlinecode"><span class="id" type="var">T_Abs</span></span> and <span class="inlinecode"><span class="id" type="var">T_RNil</span></span> are vacuous because
     abstractions and <span class="inlinecode">{}</span> don't step.  Case <span class="inlinecode"><span class="id" type="var">T_Var</span></span> is vacuous as well,
     since the context is empty.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If the final step of the derivation is by <span class="inlinecode"><span class="id" type="var">T_App</span></span>, then there
       are terms <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> and types <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span> such that <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span>,
       <span class="inlinecode"><span class="id" type="var">T</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span>, <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span> and <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span>.

<div class="paragraph"> </div>

       By inspection of the definition of the step relation, there are
       three ways <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> can step.  Cases <span class="inlinecode"><span class="id" type="var">ST_App1</span></span> and <span class="inlinecode"><span class="id" type="var">ST_App2</span></span>
       follow immediately by the induction hypotheses for the typing
       subderivations and a use of <span class="inlinecode"><span class="id" type="var">T_App</span></span>.

<div class="paragraph"> </div>

       Suppose instead <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">t<sub>2</sub></span></span> steps by <span class="inlinecode"><span class="id" type="var">ST_AppAbs</span></span>.  Then
       <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode">\<span class="id" type="var">x</span>:<span class="id" type="var">S.t12</span></span> for some type <span class="inlinecode"><span class="id" type="var">S</span></span> and term <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span>, and
       <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode">=</span> <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">t<sub>2</sub></span>]<span class="id" type="var">t<sub>12</sub></span></span>.

<div class="paragraph"> </div>

       By Lemma <span class="inlinecode"><span class="id" type="var">abs_arrow</span></span>, we have <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">S</span></span> and <span class="inlinecode"><span class="id" type="var">x</span>:<span class="id" type="var">S<sub>1</sub></span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span>.
       It then follows by lemma <span class="inlinecode"><span class="id" type="var">substitution_preserves_typing</span></span> that
       <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode">[<span class="id" type="var">x</span>:=<span class="id" type="var">t<sub>2</sub></span>]</span> <span class="inlinecode"><span class="id" type="var">t<sub>12</sub></span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span> as desired.

<div class="paragraph"> </div>


</li>
<li> If the final step of the derivation is by <span class="inlinecode"><span class="id" type="var">T_Proj</span></span>, then there
       is a term <span class="inlinecode"><span class="id" type="var">tr</span></span>, type <span class="inlinecode"><span class="id" type="var">Tr</span></span> and label <span class="inlinecode"><span class="id" type="var">i</span></span> such that <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">tr.i</span></span>,
       <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">tr</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">Tr</span></span>, and <span class="inlinecode"><span class="id" type="var">Tlookup</span></span> <span class="inlinecode"><span class="id" type="var">i</span></span> <span class="inlinecode"><span class="id" type="var">Tr</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">Some</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span>.

<div class="paragraph"> </div>

       The IH for the typing derivation gives us that, for any term
       <span class="inlinecode"><span class="id" type="var">tr'</span></span>, if <span class="inlinecode"><span class="id" type="var">tr</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">tr'</span></span> then <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">tr'</span></span> <span class="inlinecode"><span class="id" type="var">Tr</span></span>.  Inspection of
       the definition of the step relation reveals that there are two
       ways a projection can step.  Case <span class="inlinecode"><span class="id" type="var">ST_Proj1</span></span> follows
       immediately by the IH.

<div class="paragraph"> </div>

       Instead suppose <span class="inlinecode"><span class="id" type="var">tr.i</span></span> steps by <span class="inlinecode"><span class="id" type="var">ST_ProjRcd</span></span>.  Then <span class="inlinecode"><span class="id" type="var">tr</span></span> is a
       value and there is some term <span class="inlinecode"><span class="id" type="var">vi</span></span> such that
       <span class="inlinecode"><span class="id" type="var">tlookup</span></span> <span class="inlinecode"><span class="id" type="var">i</span></span> <span class="inlinecode"><span class="id" type="var">tr</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">Some</span></span> <span class="inlinecode"><span class="id" type="var">vi</span></span> and <span class="inlinecode"><span class="id" type="var">t'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">vi</span></span>.  But by lemma
       <span class="inlinecode"><span class="id" type="var">lookup_field_in_value</span></span>, <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">vi</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">Ti</span></span> as desired.

<div class="paragraph"> </div>


</li>
<li> If the final step of the derivation is by <span class="inlinecode"><span class="id" type="var">T_Sub</span></span>, then there
       is a type <span class="inlinecode"><span class="id" type="var">S</span></span> such that <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">&lt;:</span> <span class="inlinecode"><span class="id" type="var">T</span></span> and <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">S</span></span>.  The
       result is immediate by the induction hypothesis for the typing
       subderivation and an application of <span class="inlinecode"><span class="id" type="var">T_Sub</span></span>.

<div class="paragraph"> </div>


</li>
<li> If the final step of the derivation is by <span class="inlinecode"><span class="id" type="var">T_RCons</span></span>, then there
       exist some terms <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">tr</span></span>, types <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">Tr</span></span> and a label <span class="inlinecode"><span class="id" type="var">t</span></span> such
       that <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode">{<span class="id" type="var">i</span>=<span class="id" type="var">t<sub>1</sub></span>,</span> <span class="inlinecode"><span class="id" type="var">tr</span>}</span>, <span class="inlinecode"><span class="id" type="var">T</span></span> <span class="inlinecode">=</span> <span class="inlinecode">{<span class="id" type="var">i</span>:<span class="id" type="var">T<sub>1</sub></span>,</span> <span class="inlinecode"><span class="id" type="var">Tr</span>}</span>, <span class="inlinecode"><span class="id" type="var">record_ty</span></span> <span class="inlinecode"><span class="id" type="var">tr</span></span>,
       <span class="inlinecode"><span class="id" type="var">record_tm</span></span> <span class="inlinecode"><span class="id" type="var">Tr</span></span>, <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">tr</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">Tr</span></span>.

<div class="paragraph"> </div>

       By the definition of the step relation, <span class="inlinecode"><span class="id" type="var">t</span></span> must have stepped
       by <span class="inlinecode"><span class="id" type="var">ST_Rcd_Head</span></span> or <span class="inlinecode"><span class="id" type="var">ST_Rcd_Tail</span></span>.  In the first case, the
       result follows by the IH for <span class="inlinecode"><span class="id" type="var">t<sub>1</sub></span></span>'s typing derivation and
       <span class="inlinecode"><span class="id" type="var">T_RCons</span></span>.  In the second case, the result follows by the IH
       for <span class="inlinecode"><span class="id" type="var">tr</span></span>'s typing derivation, <span class="inlinecode"><span class="id" type="var">T_RCons</span></span>, and a use of the
       <span class="inlinecode"><span class="id" type="var">step_preserves_record_tm</span></span> lemma. 
</li>
</ul>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Thu&nbsp;Feb&nbsp;7&nbsp;20:09:26&nbsp;EST&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>